COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(wipe-out)
C00003 00003	EKL did it first, but cannot do it now
C00004 00004	PDL-OVERFLOW occurs also at line 3 of the proof DIAGONALIZE in the file 
C00005 ENDMK
C⊗;
(wipe-out)
(get-proofs mult)

(proof multsum)

(ue (phi |λu. disj_pair(a,b)⊃mult(u,a∪b)=mult(u,a)+mult(u,b)|) listinduction
    (part 1 (open mult union disj_pair emptyp intersection) 
            (use normal mode: always))
        (part 1 (der)) )
(label multsum)

(setq rewritemessages t)
;EKL did it first, but cannot do it now
(wipe-out)
(get-proofs sums)
(proof unionprop)

(setq rewritemessages t)

(ue (a |λn.n≤length u⊃
                (un(λm.mkset(nth(u,m)),n))(x)≡some(n,λk.nth(u,k)=x)|)
    proof_by_induction (part 1(open un mkset nth some union emptyset) (der))
    (use trans_lesseq succ_lesseq_lesseq))
;∀N.N≤LENGTH U⊃(UN(λM.MKSET(NTH(U,M)),N))(X)≡SOME(N,λK.NTH(U,K)=X)

;;PDL-OVERFLOW
QUIT


;;PDL-OVERFLOW occurs also at line 3 of the proof DIAGONALIZE in the file 
;ramsey[ekl,sys]